--------------------------------------------------------------------------------
--
--  Murphi Model of the HyperWall Architecture
--
--------------------------------------------------------------------------------
--
--  version:      0.001
--
--  written by:   Jakub Szefer
--  date:         June 2012
--  affiliation:  Princeton University (Ph.D. student)
--
--------------------------------------------------------------------------------
--
--  Model of VM terminate internal protocol
--
--
-- 
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
-- constants, types and variables
--------------------------------------------------------------------------------


-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
const
  
  NumCIPs:         1;
  NumPROCs:        1;
  NumHVs:          1;
  NumDRAMs:        1;

  NumPages:	       10;
  MaxVal:          1;

  DramMemory:      10;
  CipMemory:       10;


-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
type

  CipId:          scalarset (NumCIPs);
  DramId:         scalarset (NumDRAMs);
  ProcId:         scalarset (NumPROCs);
  HypervisorId:   scalarset (NumHVs);

  CipPageId:          scalarset (NumPages);
  DramPageId:         scalarset (NumPages);

  Val: 0..MaxVal;


  StoredState : record
    StateValue:  Val; 
  end;
 
  DramPage : record
    mem: multiset[DramMemory] of StoredState; 
  end;

  CipPage : record
    mem: multiset[CipMemory] of StoredState; 
  end;


  GlobalStates : enum {
    INIT1,
    INIT2,
		RUN1,
    RUN2,
		DONE
  };
 

-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
var

  globalState:  GlobalStates;

  dram: array[DramId] of DramPage;
  cip:  array[CipId] of CipPage; 

  value0: Val;
  value1: Val;

--------------------------------------------------------------------------------
-- funcations
--------------------------------------------------------------------------------

-- none




--------------------------------------------------------------------------------
-- states of the system (rules)
--------------------------------------------------------------------------------



-- Zeroing out of DRAM

ruleset d: DramId do
  ruleset p: DramPageId do
    rule "Zeroing out of DRAM"
      globalState = RUN1 &
      multisetcount( i : dram[d].mem, dram[d].mem[i].StateValue = 1) < DramMemory
    ==>

    var
      st : StoredState;

    begin 

      st.StateValue := 0;

      -- mark memory page as cleared
			multisetadd(st, dram[d].mem);

      -- next-state
      if( multisetcount( i : dram[d].mem, dram[d].mem[i].StateValue = 1) = DramMemory ) then
         globalState := RUN2;
      end;
      
    end;

  end;
end;


-- Clean up CIP entries

ruleset c: CipId do
  ruleset p: CipPageId do
    rule "Clearing CIP entries"
      globalState = RUN2 &
      multisetcount( i : cip[c].mem, cip[c].mem[i].StateValue = 1) < CipMemory
    ==>

    var
      st : StoredState;

    begin 

      st.StateValue := 0;

      -- mark memory page as cleared
			multisetadd(st, cip[c].mem);

      -- next-state
      if( multisetcount( i : cip[c].mem, cip[c].mem[i].StateValue = 1) = CipMemory ) then
         globalState := DONE;
      end;
      
    end;

  end;
end;






--------------------------------------------------------------------------------
-- startstate
--------------------------------------------------------------------------------

startstate

  globalState := INIT1;

  value0 := 0;
  value1 := 1;

  -- initialize DRAM
  undefine dram;

  -- initialze CIP
  undefine cip; 
 

end;




--------------------------------------------------------------------------------
-- initialization states of the system
--------------------------------------------------------------------------------


-- Initialize various memories

ruleset d: DramId do
 ruleset p: DramPageId do
   rule "Set the initial memory of the system to contain protected values, encoding 1"
      globalState = INIT1
   ==>
   var
      st : StoredState;

	 begin

      st.StateValue := 1;

	    -- pre-fill DRAM with protected pages (encoding "1")
			multisetadd(st, dram[d].mem);

      if( multisetcount( i : dram[d].mem, dram[d].mem[i].StateValue = 1) = DramMemory ) then
         globalState := INIT2;
      end;


   end;
 end;
end;


ruleset c: CipId do
 ruleset p: CipPageId do
   rule "Set the initial CIP memory of the system to contain in-use values, encoding 1"
      globalState = INIT2
   ==>
    var
      st : StoredState;

    begin 

      st.StateValue := 1;

      -- pre-fill CIP with in-use entries (encoding "1")
			multisetadd(st, cip[c].mem);

      if( multisetcount( i : cip[c].mem, cip[c].mem[i].StateValue = 1) = CipMemory ) then
         globalState := RUN1;
      end;


   end;
 end;
end;






--------------------------------------------------------------------------------
-- invariants
--------------------------------------------------------------------------------

invariant "protected pages belonging to the VM are zeroed out" 
  forall d : DramId do
	  globalState = DONE
		->
    multisetcount( i:dram[d].mem, dram[d].mem[i].StateValue = 1) = 0 -- make sure there are no pages left not zeroed out (encoded as "1")
  end;

invariant "all pages are removed from the CIP tables"
  forall c : CipId do
	  globalState = DONE
		->
    multisetcount( i:cip[c].mem, cip[c].mem[i].StateValue = 1) = 0 -- make sure there are no pages left not removed from CIP (encoded as "1")
  end;






